type name;
type ref;
const unique null : ref;
type real;
type elements;
type struct;
type exposeVersionType;
var $Heap : <x>[ref, name]x where IsHeap($Heap);
function IsHeap(h : <x>[ref, name]x) returns ($$unnamed~a : bool);
const $allocated : name;
const $elements : name;
const $inv : name;
const $localinv : name;
const $exposeVersion : name;
axiom (DeclType($exposeVersion) == System.Object);
const $sharingMode : name;
const $SharingMode_Unshared : name;
const $SharingMode_LockProtected : name;
const $ownerRef : name;
const $ownerFrame : name;
const $PeerGroupPlaceholder : name;
function ClassRepr(class : name) returns ($$unnamed~b : ref);
axiom (forall c0 : name, c1 : name :: {ClassRepr(c0), ClassRepr(c1)} ((c0 != c1) ==> (ClassRepr(c0) != ClassRepr(c1))));
axiom (forall T : name :: !($typeof(ClassRepr(T)) <: System.Object));
axiom (forall T : name :: (ClassRepr(T) != null));
axiom (forall T : name, h : <x>[ref, name]x :: {h[ClassRepr(T), $ownerFrame]} (IsHeap(h) ==> (h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder)));
function IsDirectlyModifiableField(f : name) returns ($$unnamed~c : bool);
axiom !IsDirectlyModifiableField($allocated);
axiom IsDirectlyModifiableField($elements);
axiom !IsDirectlyModifiableField($inv);
axiom !IsDirectlyModifiableField($localinv);
axiom !IsDirectlyModifiableField($ownerRef);
axiom !IsDirectlyModifiableField($ownerFrame);
axiom !IsDirectlyModifiableField($exposeVersion);
function IsStaticField(f : name) returns ($$unnamed~d : bool);
axiom !IsStaticField($allocated);
axiom !IsStaticField($elements);
axiom !IsStaticField($inv);
axiom !IsStaticField($localinv);
axiom !IsStaticField($exposeVersion);
function ValueArrayGet<any>($$unnamed~f : elements, $$unnamed~e : int) returns ($$unnamed~g : any);
function ValueArraySet<any>($$unnamed~j : elements, $$unnamed~i : int, $$unnamed~h : any) returns ($$unnamed~k : elements);
function RefArrayGet($$unnamed~m : elements, $$unnamed~l : int) returns ($$unnamed~n : ref);
function RefArraySet($$unnamed~q : elements, $$unnamed~p : int, $$unnamed~o : ref) returns ($$unnamed~r : elements);
axiom (forall<any> A : elements, i : int, x : any :: (ValueArrayGet(ValueArraySet(A, i, x), i) == x));
axiom (forall<any> A : elements, i : int, j : int, x : any :: ((i != j) ==> (ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j))));
axiom (forall A : elements, i : int, x : ref :: (RefArrayGet(RefArraySet(A, i, x), i) == x));
axiom (forall A : elements, i : int, j : int, x : ref :: ((i != j) ==> (RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j))));
function ArrayIndex(arr : ref, dim : int, indexAtDim : int, remainingIndexContribution : int) returns ($$unnamed~s : int);
axiom (forall a : ref, d : int, x : int, y : int, x' : int, y' : int :: {ArrayIndex(a, d, x, y), ArrayIndex(a, d, x', y')} ((ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y')) ==> ((x == x') && (y == y'))));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: RefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: RefArray(T, r))) ==> $Is(RefArrayGet(heap[a, $elements], i), T)));
axiom (forall a : ref, T : name, i : int, r : int, heap : <x>[ref, name]x :: {($typeof(a) <: NonNullRefArray(T, r)), RefArrayGet(heap[a, $elements], i)} ((IsHeap(heap) && ($typeof(a) <: NonNullRefArray(T, r))) ==> $IsNotNull(RefArrayGet(heap[a, $elements], i), T)));
function $Rank($$unnamed~t : ref) returns ($$unnamed~u : int);
axiom (forall a : ref :: (1 <= $Rank(a)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: RefArray(T, r))} (((a != null) && ($typeof(a) <: RefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: NonNullRefArray(T, r))} (((a != null) && ($typeof(a) <: NonNullRefArray(T, r))) ==> ($Rank(a) == r)));
axiom (forall a : ref, T : name, r : int :: {($typeof(a) <: ValueArray(T, r))} (((a != null) && ($typeof(a) <: ValueArray(T, r))) ==> ($Rank(a) == r)));
function $Length($$unnamed~v : ref) returns ($$unnamed~w : int);
axiom (forall a : ref :: {$Length(a)} (0 <= $Length(a)));
function $DimLength($$unnamed~y : ref, $$unnamed~x : int) returns ($$unnamed~z : int);
axiom (forall a : ref, i : int :: (0 <= $DimLength(a, i)));
axiom (forall a : ref :: {$DimLength(a, 0)} (($Rank(a) == 1) ==> ($DimLength(a, 0) == $Length(a))));
function $LBound($$unnamed~ab : ref, $$unnamed~aa : int) returns ($$unnamed~ac : int);
function $UBound($$unnamed~ae : ref, $$unnamed~ad : int) returns ($$unnamed~af : int);
axiom (forall a : ref, i : int :: {$LBound(a, i)} ($LBound(a, i) == 0));
axiom (forall a : ref, i : int :: {$UBound(a, i)} ($UBound(a, i) == ($DimLength(a, i) - 1)));
const $ArrayCategoryValue : name;
const $ArrayCategoryRef : name;
const $ArrayCategoryNonNullRef : name;
function $ArrayCategory(arrayType : name) returns (arrayCategory : name);
axiom (forall T : name, ET : name, r : int :: {(T <: ValueArray(ET, r))} ((T <: ValueArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryValue)));
axiom (forall T : name, ET : name, r : int :: {(T <: RefArray(ET, r))} ((T <: RefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryRef)));
axiom (forall T : name, ET : name, r : int :: {(T <: NonNullRefArray(ET, r))} ((T <: NonNullRefArray(ET, r)) ==> ($ArrayCategory(T) == $ArrayCategoryNonNullRef)));
const System.Array : name;
axiom (System.Array <: System.Object);
function $ElementType($$unnamed~ag : name) returns ($$unnamed~ah : name);
function ValueArray(elementType : name, rank : int) returns ($$unnamed~ai : name);
axiom (forall T : name, r : int :: {ValueArray(T, r)} (ValueArray(T, r) <: System.Array));
function RefArray(elementType : name, rank : int) returns ($$unnamed~aj : name);
axiom (forall T : name, r : int :: {RefArray(T, r)} (RefArray(T, r) <: System.Array));
function NonNullRefArray(elementType : name, rank : int) returns ($$unnamed~ak : name);
axiom (forall T : name, r : int :: {NonNullRefArray(T, r)} (NonNullRefArray(T, r) <: System.Array));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (RefArray(U, r) <: RefArray(T, r))));
axiom (forall T : name, U : name, r : int :: ((U <: T) ==> (NonNullRefArray(U, r) <: NonNullRefArray(T, r))));
axiom (forall A : name, r : int :: ($ElementType(ValueArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(RefArray(A, r)) == A));
axiom (forall A : name, r : int :: ($ElementType(NonNullRefArray(A, r)) == A));
axiom (forall A : name, r : int, T : name :: {(T <: RefArray(A, r))} ((T <: RefArray(A, r)) ==> ((T == RefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: NonNullRefArray(A, r))} ((T <: NonNullRefArray(A, r)) ==> ((T == NonNullRefArray($ElementType(T), r)) && ($ElementType(T) <: A))));
axiom (forall A : name, r : int, T : name :: {(T <: ValueArray(A, r))} ((T <: ValueArray(A, r)) ==> (T == ValueArray(A, r))));
axiom (forall A : name, r : int, T : name :: ((RefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == RefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((NonNullRefArray(A, r) <: T) ==> ((System.Array <: T) || ((T == NonNullRefArray($ElementType(T), r)) && (A <: $ElementType(T))))));
axiom (forall A : name, r : int, T : name :: ((ValueArray(A, r) <: T) ==> ((System.Array <: T) || (T == ValueArray(A, r)))));
function $ArrayPtr(elementType : name) returns ($$unnamed~al : name);
function $StructGet<any>($$unnamed~an : struct, $$unnamed~am : name) returns ($$unnamed~ao : any);
function $StructSet<any>($$unnamed~ar : struct, $$unnamed~aq : name, $$unnamed~ap : any) returns ($$unnamed~as : struct);
axiom (forall<any> s : struct, f : name, x : any :: ($StructGet($StructSet(s, f, x), f) == x));
axiom (forall<any> s : struct, f : name, f' : name, x : any :: ((f != f') ==> ($StructGet($StructSet(s, f, x), f') == $StructGet(s, f'))));
function ZeroInit(s : struct, typ : name) returns ($$unnamed~at : bool);
function $typeof($$unnamed~au : ref) returns ($$unnamed~av : name);
function $BaseClass(sub : name) returns (base : name);
function AsDirectSubClass(sub : name, base : name) returns (sub' : name);
function OneClassDown(sub : name, base : name) returns (directSub : name);
axiom (forall A : name, B : name, C : name :: {(C <: AsDirectSubClass(B, A))} ((C <: AsDirectSubClass(B, A)) ==> (OneClassDown(C, A) == B)));
function $IsValueType($$unnamed~aw : name) returns ($$unnamed~ax : bool);
axiom (forall T : name :: ($IsValueType(T) ==> ((forall U : name :: ((T <: U) ==> (T == U))) && (forall U : name :: ((U <: T) ==> (T == U))))));
const System.Object : name;
function $IsTokenForType($$unnamed~az : struct, $$unnamed~ay : name) returns ($$unnamed~ba : bool);
function TypeObject($$unnamed~bb : name) returns ($$unnamed~bc : ref);
const System.Type : name;
axiom (System.Type <: System.Object);
axiom (forall T : name :: {TypeObject(T)} $IsNotNull(TypeObject(T), System.Type));
function TypeName($$unnamed~bd : ref) returns ($$unnamed~be : name);
axiom (forall T : name :: {TypeObject(T)} (TypeName(TypeObject(T)) == T));
function $Is($$unnamed~bg : ref, $$unnamed~bf : name) returns ($$unnamed~bh : bool);
axiom (forall o : ref, T : name :: {$Is(o, T)} ($Is(o, T) <==> ((o == null) || ($typeof(o) <: T))));
function $IsNotNull($$unnamed~bj : ref, $$unnamed~bi : name) returns ($$unnamed~bk : bool);
axiom (forall o : ref, T : name :: {$IsNotNull(o, T)} ($IsNotNull(o, T) <==> ((o != null) && $Is(o, T))));
function $As($$unnamed~bm : ref, $$unnamed~bl : name) returns ($$unnamed~bn : ref);
axiom (forall o : ref, T : name :: ($Is(o, T) ==> ($As(o, T) == o)));
axiom (forall o : ref, T : name :: (!$Is(o, T) ==> ($As(o, T) == null)));
axiom (forall h : <x>[ref, name]x, o : ref :: {($typeof(o) <: System.Array), h[o, $inv]} (((IsHeap(h) && (o != null)) && ($typeof(o) <: System.Array)) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
function IsAllocated<any>(h : <x>[ref, name]x, o : any) returns ($$unnamed~bo : bool);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {IsAllocated(h, h[o, f])} ((IsHeap(h) && h[o, $allocated]) ==> IsAllocated(h, h[o, f])));
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[h[o, f], $allocated]} ((IsHeap(h) && h[o, $allocated]) ==> h[h[o, f], $allocated]));
axiom (forall h : <x>[ref, name]x, s : struct, f : name :: {IsAllocated(h, $StructGet(s, f))} (IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, RefArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, e : elements, i : int :: {IsAllocated(h, ValueArrayGet(e, i))} (IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))));
axiom (forall h : <x>[ref, name]x, o : ref :: {h[o, $allocated]} (IsAllocated(h, o) ==> h[o, $allocated]));
axiom (forall h : <x>[ref, name]x, c : name :: {h[ClassRepr(c), $allocated]} (IsHeap(h) ==> h[ClassRepr(c), $allocated]));
const $BeingConstructed : ref;
const $NonNullFieldsAreInitialized : name;
function DeclType(field : name) returns (class : name);
function AsNonNullRefField(field : name, T : name) returns (f : name);
function AsRefField(field : name, T : name) returns (f : name);
function AsRangeField(field : name, T : name) returns (f : name);
axiom (forall f : name, T : name :: {AsNonNullRefField(f, T)} ((AsNonNullRefField(f, T) == f) ==> (AsRefField(f, T) == f)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRefField(f, T)]} (IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsNonNullRefField(f, T)]} (((IsHeap(h) && (o != null)) && ((o != $BeingConstructed) || (h[$BeingConstructed, $NonNullFieldsAreInitialized] == true))) ==> (h[o, AsNonNullRefField(f, T)] != null)));
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRangeField(f, T)]} (IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)));
function $IsMemberlessType($$unnamed~bp : name) returns ($$unnamed~bq : bool);
axiom (forall o : ref :: {$IsMemberlessType($typeof(o))} !$IsMemberlessType($typeof(o)));
function $IsImmutable(T : name) returns ($$unnamed~br : bool);
axiom !$IsImmutable(System.Object);
function $AsImmutable(T : name) returns (theType : name);
function $AsMutable(T : name) returns (theType : name);
axiom (forall T : name, U : name :: {(U <: $AsImmutable(T))} ((U <: $AsImmutable(T)) ==> ($IsImmutable(U) && ($AsImmutable(U) == U))));
axiom (forall T : name, U : name :: {(U <: $AsMutable(T))} ((U <: $AsMutable(T)) ==> (!$IsImmutable(U) && ($AsMutable(U) == U))));
function AsOwner(string : ref, owner : ref) returns (theString : ref);
axiom (forall o : ref, T : name :: {($typeof(o) <: $AsImmutable(T))} ((((o != null) && (o != $BeingConstructed)) && ($typeof(o) <: $AsImmutable(T))) ==> (forall h : <x>[ref, name]x :: {IsHeap(h)} (IsHeap(h) ==> (((((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o))) && (h[o, $ownerFrame] == $PeerGroupPlaceholder)) && (AsOwner(o, h[o, $ownerRef]) == o)) && (forall t : ref :: {AsOwner(o, h[t, $ownerRef])} ((AsOwner(o, h[t, $ownerRef]) == o) ==> ((t == o) || (h[t, $ownerFrame] != $PeerGroupPlaceholder)))))))));
const System.String : name;
function $StringLength($$unnamed~bs : ref) returns ($$unnamed~bt : int);
axiom (forall s : ref :: {$StringLength(s)} (0 <= $StringLength(s)));
function AsRepField(f : name, declaringType : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name, T : name :: {h[o, AsRepField(f, T)]} ((IsHeap(h) && (h[o, AsRepField(f, T)] != null)) ==> ((h[h[o, AsRepField(f, T)], $ownerRef] == o) && (h[h[o, AsRepField(f, T)], $ownerFrame] == T))));
function AsPeerField(f : name) returns (theField : name);
axiom (forall h : <x>[ref, name]x, o : ref, f : name :: {h[o, AsPeerField(f)]} ((IsHeap(h) && (h[o, AsPeerField(f)] != null)) ==> ((h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef]) && (h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]))));
axiom (forall h : <x>[ref, name]x, o : ref :: {(h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])} ((((IsHeap(h) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> ((h[o, $inv] == $typeof(o)) && (h[o, $localinv] == $typeof(o)))));
procedure $SetOwner(o : ref, ow : ref, fr : name);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[o, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[o, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == ow) && ($Heap[p, $ownerFrame] == fr))));
  

procedure $UpdateOwnersForRep(o : ref, T : name, e : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} (((((F != $ownerRef) && (F != $ownerFrame)) || old(($Heap[p, $ownerRef] != $Heap[e, $ownerRef]))) || old(($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((e == null) ==> ($Heap == old($Heap)));
  ensures ((e != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} ((old(($Heap[p, $ownerRef] == $Heap[e, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]))) ==> (($Heap[p, $ownerRef] == o) && ($Heap[p, $ownerFrame] == T)))));
  

procedure $UpdateOwnersForPeer(c : ref, d : ref);
  modifies $Heap;
  ensures (forall p : ref, F : name :: {$Heap[p, F]} ((((F != $ownerRef) && (F != $ownerFrame)) || old(((($Heap[p, $ownerRef] != $Heap[c, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[c, $ownerFrame])) && (($Heap[p, $ownerRef] != $Heap[d, $ownerRef]) || ($Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]))))) ==> (old($Heap[p, F]) == $Heap[p, F])));
  ensures ((d == null) ==> ($Heap == old($Heap)));
  ensures ((d != null) ==> (forall p : ref :: {$Heap[p, $ownerRef]} {$Heap[p, $ownerFrame]} (((old(($Heap[p, $ownerRef] == $Heap[c, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[c, $ownerFrame]))) || (old(($Heap[p, $ownerRef] == $Heap[d, $ownerRef])) && old(($Heap[p, $ownerFrame] == $Heap[d, $ownerFrame])))) ==> ((((old($Heap)[d, $ownerFrame] == $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[c, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame])) || (((old($Heap)[d, $ownerFrame] != $PeerGroupPlaceholder) && ($Heap[p, $ownerRef] == old($Heap)[d, $ownerRef])) && ($Heap[p, $ownerFrame] == old($Heap)[d, $ownerFrame]))))));
  

const $FirstConsistentOwner : name;
function $AsPureObject($$unnamed~bu : ref) returns ($$unnamed~bv : ref);
function ##FieldDependsOnFCO<any>(o : ref, f : name, ev : exposeVersionType) returns (value : any);
axiom (forall o : ref, f : name, h : <x>[ref, name]x :: {h[$AsPureObject(o), f]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion]))));
axiom (forall o : ref, h : <x>[ref, name]x :: {h[o, $FirstConsistentOwner]} ((((((IsHeap(h) && (o != null)) && (h[o, $allocated] == true)) && (h[o, $ownerFrame] != $PeerGroupPlaceholder)) && (h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame])) && (h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]))) ==> (((h[o, $FirstConsistentOwner] != null) && (h[h[o, $FirstConsistentOwner], $allocated] == true)) && (((h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder) || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame])) || (h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))))));
function Box<any>($$unnamed~bx : any, $$unnamed~bw : ref) returns ($$unnamed~by : ref);
function Unbox<any>($$unnamed~bz : ref) returns ($$unnamed~ca : any);
axiom (forall<any> x : any, p : ref :: {Unbox(Box(x, p))} (Unbox(Box(x, p)) == x));
function UnboxedType($$unnamed~cb : ref) returns ($$unnamed~cc : name);
axiom (forall p : ref :: {$IsValueType(UnboxedType(p))} ($IsValueType(UnboxedType(p)) ==> (forall<any> heap : <x>[ref, name]x, x : any :: {heap[Box(x, p), $inv]} (IsHeap(heap) ==> ((heap[Box(x, p), $inv] == $typeof(Box(x, p))) && (heap[Box(x, p), $localinv] == $typeof(Box(x, p))))))));
axiom (forall<any> x : any, p : ref :: {(UnboxedType(Box(x, p)) <: System.Object)} (((UnboxedType(Box(x, p)) <: System.Object) && (Box(x, p) == p)) ==> (x == p)));
function BoxTester(p : ref, typ : name) returns ($$unnamed~cd : ref);
axiom (forall p : ref, typ : name :: {BoxTester(p, typ)} ((UnboxedType(p) == typ) <==> (BoxTester(p, typ) != null)));
const System.SByte : name;
axiom $IsValueType(System.SByte);
const System.Byte : name;
axiom $IsValueType(System.Byte);
const System.Int16 : name;
axiom $IsValueType(System.Int16);
const System.UInt16 : name;
axiom $IsValueType(System.UInt16);
const System.Int32 : name;
axiom $IsValueType(System.Int32);
const System.UInt32 : name;
axiom $IsValueType(System.UInt32);
const System.Int64 : name;
axiom $IsValueType(System.Int64);
const System.UInt64 : name;
axiom $IsValueType(System.UInt64);
const System.Char : name;
axiom $IsValueType(System.Char);
const int#m2147483648 : int;
const int#2147483647 : int;
const int#4294967295 : int;
const int#m9223372036854775808 : int;
const int#9223372036854775807 : int;
const int#18446744073709551615 : int;
axiom (int#m9223372036854775808 < int#m2147483648);
axiom (int#m2147483648 < (0 - 100000));
axiom (100000 < int#2147483647);
axiom (int#2147483647 < int#4294967295);
axiom (int#4294967295 < int#9223372036854775807);
axiom (int#9223372036854775807 < int#18446744073709551615);
function InRange(i : int, T : name) returns ($$unnamed~ce : bool);
axiom (forall i : int :: (InRange(i, System.SByte) <==> (((0 - 128) <= i) && (i < 128))));
axiom (forall i : int :: (InRange(i, System.Byte) <==> ((0 <= i) && (i < 256))));
axiom (forall i : int :: (InRange(i, System.Int16) <==> (((0 - 32768) <= i) && (i < 32768))));
axiom (forall i : int :: (InRange(i, System.UInt16) <==> ((0 <= i) && (i < 65536))));
axiom (forall i : int :: (InRange(i, System.Int32) <==> ((int#m2147483648 <= i) && (i <= int#2147483647))));
axiom (forall i : int :: (InRange(i, System.UInt32) <==> ((0 <= i) && (i <= int#4294967295))));
axiom (forall i : int :: (InRange(i, System.Int64) <==> ((int#m9223372036854775808 <= i) && (i <= int#9223372036854775807))));
axiom (forall i : int :: (InRange(i, System.UInt64) <==> ((0 <= i) && (i <= int#18446744073709551615))));
axiom (forall i : int :: (InRange(i, System.Char) <==> ((0 <= i) && (i < 65536))));
function $IntToInt(val : int, fromType : name, toType : name) returns ($$unnamed~cf : int);
function $IntToReal($$unnamed~cg : int, fromType : name, toType : name) returns ($$unnamed~ch : real);
function $RealToInt($$unnamed~ci : real, fromType : name, toType : name) returns ($$unnamed~cj : int);
function $RealToReal(val : real, fromType : name, toType : name) returns ($$unnamed~ck : real);
function $SizeIs($$unnamed~cm : name, $$unnamed~cl : int) returns ($$unnamed~cn : bool);
function $IfThenElse<any>($$unnamed~cq : bool, $$unnamed~cp : any, $$unnamed~co : any) returns ($$unnamed~cr : any);
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (b ==> ($IfThenElse(b, x, y) == x)));
axiom (forall<any> b : bool, x : any, y : any :: {$IfThenElse(b, x, y)} (!b ==> ($IfThenElse(b, x, y) == y)));
function #neg($$unnamed~cs : int) returns ($$unnamed~ct : int);
function #and($$unnamed~cv : int, $$unnamed~cu : int) returns ($$unnamed~cw : int);
function #or($$unnamed~cy : int, $$unnamed~cx : int) returns ($$unnamed~cz : int);
function #xor($$unnamed~db : int, $$unnamed~da : int) returns ($$unnamed~dc : int);
function #shl($$unnamed~de : int, $$unnamed~dd : int) returns ($$unnamed~df : int);
function #shr($$unnamed~dh : int, $$unnamed~dg : int) returns ($$unnamed~di : int);
function #rneg($$unnamed~dj : real) returns ($$unnamed~dk : real);
function #radd($$unnamed~dm : real, $$unnamed~dl : real) returns ($$unnamed~dn : real);
function #rsub($$unnamed~dp : real, $$unnamed~do : real) returns ($$unnamed~dq : real);
function #rmul($$unnamed~ds : real, $$unnamed~dr : real) returns ($$unnamed~dt : real);
function #rdiv($$unnamed~dv : real, $$unnamed~du : real) returns ($$unnamed~dw : real);
function #rmod($$unnamed~dy : real, $$unnamed~dx : real) returns ($$unnamed~dz : real);
function #rLess($$unnamed~eb : real, $$unnamed~ea : real) returns ($$unnamed~ec : bool);
function #rAtmost($$unnamed~ee : real, $$unnamed~ed : real) returns ($$unnamed~ef : bool);
function #rEq($$unnamed~eh : real, $$unnamed~eg : real) returns ($$unnamed~ei : bool);
function #rNeq($$unnamed~ek : real, $$unnamed~ej : real) returns ($$unnamed~el : bool);
function #rAtleast($$unnamed~en : real, $$unnamed~em : real) returns ($$unnamed~eo : bool);
function #rGreater($$unnamed~eq : real, $$unnamed~ep : real) returns ($$unnamed~er : bool);
axiom (forall x : int, y : int :: {(x % y)} {(x / y)} ((x % y) == (x - ((x / y) * y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (0 < y)) ==> ((0 <= (x % y)) && ((x % y) < y))));
axiom (forall x : int, y : int :: {(x % y)} (((0 <= x) && (y < 0)) ==> ((0 <= (x % y)) && ((x % y) < (0 - y)))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (0 < y)) ==> (((0 - y) < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {(x % y)} (((x <= 0) && (y < 0)) ==> ((y < (x % y)) && ((x % y) <= 0))));
axiom (forall x : int, y : int :: {((x + y) % y)} (((0 <= x) && (0 <= y)) ==> (((x + y) % y) == (x % y))));
axiom (forall x : int, y : int :: {((y + x) % y)} (((0 <= x) && (0 <= y)) ==> (((y + x) % y) == (x % y))));
axiom (forall x : int, y : int :: {((x - y) % y)} (((0 <= (x - y)) && (0 <= y)) ==> (((x - y) % y) == (x % y))));
axiom (forall a : int, b : int, d : int :: {(a % d), (b % d)} ((((2 <= d) && ((a % d) == (b % d))) && (a < b)) ==> ((a + d) <= b)));
axiom (forall x : int, y : int :: {#and(x, y)} (((0 <= x) || (0 <= y)) ==> (0 <= #and(x, y))));
axiom (forall x : int, y : int :: {#or(x, y)} (((0 <= x) && (0 <= y)) ==> ((0 <= #or(x, y)) && (#or(x, y) <= (x + y)))));
axiom (forall i : int :: {#shl(i, 0)} (#shl(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shl(i, (j + 1)) == (#shl(i, j) * 2))));
axiom (forall i : int :: {#shr(i, 0)} (#shr(i, 0) == i));
axiom (forall i : int, j : int :: ((0 <= j) ==> (#shr(i, (j + 1)) == (#shr(i, j) / 2))));
function #System.String.IsInterned$System.String$notnull($$unnamed~es : ref) returns ($$unnamed~et : ref);
function #System.String.Equals$System.String($$unnamed~ev : ref, $$unnamed~eu : ref) returns ($$unnamed~ew : bool);
function #System.String.Equals$System.String$System.String($$unnamed~ey : ref, $$unnamed~ex : ref) returns ($$unnamed~ez : bool);
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String(a, b)} (#System.String.Equals$System.String(a, b) == #System.String.Equals$System.String$System.String(a, b)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} (#System.String.Equals$System.String$System.String(a, b) == #System.String.Equals$System.String$System.String(b, a)));
axiom (forall a : ref, b : ref :: {#System.String.Equals$System.String$System.String(a, b)} ((((a != null) && (b != null)) && #System.String.Equals$System.String$System.String(a, b)) ==> (#System.String.IsInterned$System.String$notnull(a) == #System.String.IsInterned$System.String$notnull(b))));
const $UnknownRef : ref;
const ReturnFinally.x : name;
const ReturnFinally.y : name;
const System.Collections.IEnumerable : name;
const System.IEquatable`1...System.String : name;
const Microsoft.Contracts.ICheckedException : name;
const ReturnFinally : name;
const System.Runtime.Serialization.ISerializable : name;
const System.Runtime.InteropServices._Type : name;
const System.Exception : name;
const System.IComparable : name;
const System.Reflection.MemberInfo : name;
const System.Runtime.InteropServices._MemberInfo : name;
const System.Collections.Generic.IEnumerable`1...System.Char : name;
const System.Runtime.InteropServices._Exception : name;
const Microsoft.Contracts.ObjectInvariantException : name;
const System.Boolean : name;
const System.IComparable`1...System.String : name;
const System.Reflection.ICustomAttributeProvider : name;
const Microsoft.Contracts.GuardException : name;
const System.ICloneable : name;
const System.IConvertible : name;
const System.Reflection.IReflect : name;
axiom !IsStaticField(ReturnFinally.y);
axiom IsDirectlyModifiableField(ReturnFinally.y);
axiom (DeclType(ReturnFinally.y) == ReturnFinally);
axiom (AsRangeField(ReturnFinally.y, System.Int32) == ReturnFinally.y);
axiom IsStaticField(ReturnFinally.x);
axiom IsDirectlyModifiableField(ReturnFinally.x);
axiom (DeclType(ReturnFinally.x) == ReturnFinally);
axiom (AsRangeField(ReturnFinally.x, System.Int32) == ReturnFinally.x);
axiom (ReturnFinally <: ReturnFinally);
axiom ($BaseClass(ReturnFinally) == System.Object);
axiom ((ReturnFinally <: $BaseClass(ReturnFinally)) && (AsDirectSubClass(ReturnFinally, $BaseClass(ReturnFinally)) == ReturnFinally));
axiom (!$IsImmutable(ReturnFinally) && ($AsMutable(ReturnFinally) == ReturnFinally));
axiom (forall $oi : ref, $h : <x>[ref, name]x :: {($h[$oi, $inv] <: ReturnFinally)} (((IsHeap($h) && ($h[$oi, $inv] <: ReturnFinally)) && ($h[$oi, $localinv] != System.Object)) ==> (0 <= $h[$oi, ReturnFinally.y])));
axiom (forall $U : name :: {($U <: System.Boolean)} (($U <: System.Boolean) ==> ($U == System.Boolean)));
procedure ReturnFinally.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool where true) returns ($result : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures true;
  free ensures true;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.SpecSharp.CheckInvariant$System.Boolean(this : ref, throwException$in : bool) returns ($result : bool) {
  var throwException : bool where true;
  var stack0i : int;
  var stack1i : int;
  var stack0b : bool;
  var return.value : bool where true;
  var stack50000o : ref;
  var stack0o : ref;
  var SS$Display.Return.Local : bool where true;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~b;
  $$entry~b: assume ($Heap[this, $allocated] == true); goto $$entry~a;
  $$entry~a: throwException := throwException$in; goto block4386;
  block4386: goto block4403;
  block4403: stack0i := 0; goto $$block4403~b;
  $$block4403~b: assert (this != null); goto $$block4403~a;
  $$block4403~a: stack1i := $Heap[this, ReturnFinally.y]; goto true4403to4522, false4403to4420;
  true4403to4522: assume (stack0i <= stack1i); goto block4522;
  false4403to4420: assume (stack0i > stack1i); goto block4420;
  block4522: goto block4539;
  block4420: stack0b := throwException; goto true4420to4471, false4420to4437;
  true4420to4471: assume !stack0b; goto block4471;
  false4420to4437: assume stack0b; goto block4437;
  block4471: return.value := false; goto block4573;
  block4437: assume false; goto $$block4437~i;
  $$block4437~i: havoc stack50000o; goto $$block4437~h;
  $$block4437~h: assume ((($Heap[stack50000o, $allocated] == false) && (stack50000o != null)) && ($typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException)); goto $$block4437~g;
  $$block4437~g: assume (($Heap[stack50000o, $ownerRef] == stack50000o) && ($Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder)); goto $$block4437~f;
  $$block4437~f: $Heap := $Heap[stack50000o, $allocated := true]; goto $$block4437~e;
  $$block4437~e: assert (stack50000o != null); goto $$block4437~d;
  $$block4437~d: call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); goto $$block4437~c;
  $$block4437~c: stack0o := stack50000o; goto $$block4437~b;
  $$block4437~b: assert (stack0o != null); goto $$block4437~a;
  $$block4437~a: assume false; return;
  block4539: goto block4556;
  block4573: goto block4590;
  block4556: return.value := true; goto block4573;
  block4590: SS$Display.Return.Local := return.value; goto $$block4590~b;
  $$block4590~b: stack0b := return.value; goto $$block4590~a;
  $$block4590~a: $result := stack0b; return;
  
}

axiom (Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException);
axiom (Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException);
axiom (System.Exception <: System.Exception);
axiom ($BaseClass(System.Exception) == System.Object);
axiom ((System.Exception <: $BaseClass(System.Exception)) && (AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception));
axiom (!$IsImmutable(System.Exception) && ($AsMutable(System.Exception) == System.Exception));
axiom (System.Runtime.Serialization.ISerializable <: System.Object);
axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable);
axiom (System.Exception <: System.Runtime.Serialization.ISerializable);
axiom (System.Runtime.InteropServices._Exception <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Exception);
axiom (System.Exception <: System.Runtime.InteropServices._Exception);
axiom ($BaseClass(Microsoft.Contracts.GuardException) == System.Exception);
axiom ((Microsoft.Contracts.GuardException <: $BaseClass(Microsoft.Contracts.GuardException)) && (AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException));
axiom (!$IsImmutable(Microsoft.Contracts.GuardException) && ($AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException));
axiom ($BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException);
axiom ((Microsoft.Contracts.ObjectInvariantException <: $BaseClass(Microsoft.Contracts.ObjectInvariantException)) && (AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException));
axiom (!$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && ($AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException));
procedure Microsoft.Contracts.ObjectInvariantException..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(Microsoft.Contracts.ObjectInvariantException <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure ReturnFinally.TryFinally0(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  ensures ($Heap[ClassRepr(ReturnFinally), ReturnFinally.x] == 6);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != ClassRepr(ReturnFinally)) || ($f != ReturnFinally.x)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.TryFinally0(this : ref) {
  var stack0i : int;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~c;
  $$entry~c: assume ($Heap[this, $allocated] == true); goto block5389;
  block5389: goto block5644;
  block5644: goto block5661;
  block5661: goto block5967;
  block5967: stack0i := 10; goto $$block5967~b;
  $$block5967~b: $Heap := $Heap[ClassRepr(ReturnFinally), ReturnFinally.x := stack0i]; goto $$block5967~a;
  $$block5967~a: assume IsHeap($Heap); goto block5712;
  block5712: goto block5729;
  block5729: goto block5933;
  block5933: goto block5950;
  block5950: return;
  
}

procedure ReturnFinally.TryFinally1(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  ensures ($Heap[ClassRepr(ReturnFinally), ReturnFinally.x] == 6);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != ClassRepr(ReturnFinally)) || ($f != ReturnFinally.x)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.TryFinally1(this : ref) {
  var stack0i : int;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~d;
  $$entry~d: assume ($Heap[this, $allocated] == true); goto block6749;
  block6749: goto block7004;
  block7004: goto block7021;
  block7021: stack0i := 6; goto $$block7021~b;
  $$block7021~b: $Heap := $Heap[ClassRepr(ReturnFinally), ReturnFinally.x := stack0i]; goto $$block7021~a;
  $$block7021~a: assume IsHeap($Heap); goto block7327;
  block7327: stack0i := 10; goto $$block7327~b;
  $$block7327~b: $Heap := $Heap[ClassRepr(ReturnFinally), ReturnFinally.x := stack0i]; goto $$block7327~a;
  $$block7327~a: assume IsHeap($Heap); goto block7072;
  block7072: goto block7089;
  block7089: goto block7293;
  block7293: goto block7310;
  block7310: return;
  
}

procedure ReturnFinally.TryFinally2(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  ensures ($Heap[ClassRepr(ReturnFinally), ReturnFinally.x] == 6);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != ClassRepr(ReturnFinally)) || ($f != ReturnFinally.x)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.TryFinally2(this : ref) {
  var stack0i : int;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~e;
  $$entry~e: assume ($Heap[this, $allocated] == true); goto block8075;
  block8075: goto block8330;
  block8330: goto block8347;
  block8347: stack0i := 10; goto $$block8347~b;
  $$block8347~b: $Heap := $Heap[ClassRepr(ReturnFinally), ReturnFinally.x := stack0i]; goto $$block8347~a;
  $$block8347~a: assume IsHeap($Heap); goto block8653;
  block8653: stack0i := 6; goto $$block8653~b;
  $$block8653~b: $Heap := $Heap[ClassRepr(ReturnFinally), ReturnFinally.x := stack0i]; goto $$block8653~a;
  $$block8653~a: assume IsHeap($Heap); goto block8398;
  block8398: goto block8415;
  block8415: goto block8619;
  block8619: goto block8636;
  block8636: return;
  
}

procedure ReturnFinally.TryFinally3(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.TryFinally3(this : ref) {
  var stack0o : ref;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~f;
  $$entry~f: assume ($Heap[this, $allocated] == true); goto block9503;
  block9503: goto block9758;
  block9758: goto block9775;
  block9775: goto block9877;
  block9877: assert true; goto block9945;
  block9945: goto block9962;
  block9962: goto block9826;
  block9826: goto block9843;
  block9843: goto block9860;
  block9860: return;
  
}

axiom (System.String <: System.String);
axiom ($BaseClass(System.String) == System.Object);
axiom ((System.String <: $BaseClass(System.String)) && (AsDirectSubClass(System.String, $BaseClass(System.String)) == System.String));
axiom ($IsImmutable(System.String) && ($AsImmutable(System.String) == System.String));
axiom (System.IComparable <: System.Object);
axiom $IsMemberlessType(System.IComparable);
axiom (System.String <: System.IComparable);
axiom (System.ICloneable <: System.Object);
axiom $IsMemberlessType(System.ICloneable);
axiom (System.String <: System.ICloneable);
axiom (System.IConvertible <: System.Object);
axiom $IsMemberlessType(System.IConvertible);
axiom (System.String <: System.IConvertible);
axiom (System.IComparable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IComparable`1...System.String);
axiom (System.String <: System.IComparable`1...System.String);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Object);
axiom (System.Collections.IEnumerable <: System.Object);
axiom $IsMemberlessType(System.Collections.IEnumerable);
axiom (System.Collections.Generic.IEnumerable`1...System.Char <: System.Collections.IEnumerable);
axiom $IsMemberlessType(System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.Generic.IEnumerable`1...System.Char);
axiom (System.String <: System.Collections.IEnumerable);
axiom (System.IEquatable`1...System.String <: System.Object);
axiom $IsMemberlessType(System.IEquatable`1...System.String);
axiom (System.String <: System.IEquatable`1...System.String);
axiom (forall $U : name :: {($U <: System.String)} (($U <: System.String) ==> ($U == System.String)));
procedure ReturnFinally.Expose0$System.Boolean(this : ref, b$in : bool where true);
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.Expose0$System.Boolean(this : ref, b$in : bool) {
  var b : bool where true;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local11900 : ref where $Is(local11900, System.Exception);
  var stack0i : int;
  var stack0b : bool;
  var stack0o : ref;
  var stack0s : struct;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~h;
  $$entry~h: assume ($Heap[this, $allocated] == true); goto $$entry~g;
  $$entry~g: b := b$in; goto block10829;
  block10829: goto block11084;
  block11084: goto block11101;
  block11101: temp0 := this; goto $$block11101~j;
  $$block11101~j: havoc stack1s; goto $$block11101~i;
  $$block11101~i: assume $IsTokenForType(stack1s, ReturnFinally); goto $$block11101~h;
  $$block11101~h: stack1o := TypeObject(ReturnFinally); goto $$block11101~g;
  $$block11101~g: assert (temp0 != null); goto $$block11101~f;
  $$block11101~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: ReturnFinally)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block11101~e;
  $$block11101~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block11101~d;
  $$block11101~d: havoc temp1; goto $$block11101~c;
  $$block11101~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block11101~b;
  $$block11101~b: assume IsHeap($Heap); goto $$block11101~a;
  $$block11101~a: local11900 := null; goto block11118;
  block11118: stack0i := -4; goto $$block11118~d;
  $$block11118~d: assert (this != null); goto $$block11118~c;
  $$block11118~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block11118~b;
  $$block11118~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block11118~a;
  $$block11118~a: assume IsHeap($Heap); goto block11135;
  block11135: stack0b := b; goto true11135to11169, false11135to11152;
  true11135to11169: assume !stack0b; goto block11169;
  false11135to11152: assume stack0b; goto block11152;
  block11169: goto block11186;
  block11152: goto block11373;
  block11186: goto block11203;
  block11373: stack0o := null; goto true11373to11475, false11373to11390;
  true11373to11475: assume (local11900 == stack0o); goto block11475;
  false11373to11390: assume (local11900 != stack0o); goto block11390;
  block11475: goto block11492;
  block11390: goto true11390to11475, false11390to11407;
  block11203: stack0i := 2; goto $$block11203~d;
  $$block11203~d: assert (this != null); goto $$block11203~c;
  $$block11203~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block11203~b;
  $$block11203~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block11203~a;
  $$block11203~a: assume IsHeap($Heap); goto block11509;
  true11390to11475: assume ($As(local11900, Microsoft.Contracts.ICheckedException) != null); goto block11475;
  false11390to11407: assume ($As(local11900, Microsoft.Contracts.ICheckedException) == null); goto block11407;
  block11407: goto block11424;
  block11509: stack0o := null; goto true11509to11611, false11509to11526;
  true11509to11611: assume (local11900 == stack0o); goto block11611;
  false11509to11526: assume (local11900 != stack0o); goto block11526;
  block11611: goto block11628;
  block11526: goto true11526to11611, false11526to11543;
  block11492: havoc stack0s; goto $$block11492~h;
  $$block11492~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block11492~g;
  $$block11492~g: stack0o := TypeObject(ReturnFinally); goto $$block11492~f;
  $$block11492~f: assert (temp0 != null); goto $$block11492~e;
  $$block11492~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block11492~d;
  $$block11492~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block11492~c;
  $$block11492~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block11492~b;
  $$block11492~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block11492~a;
  $$block11492~a: assume IsHeap($Heap); goto block11424;
  true11526to11611: assume ($As(local11900, Microsoft.Contracts.ICheckedException) != null); goto block11611;
  false11526to11543: assume ($As(local11900, Microsoft.Contracts.ICheckedException) == null); goto block11543;
  block11543: goto block11560;
  block11424: goto block11441;
  block11628: havoc stack0s; goto $$block11628~h;
  $$block11628~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block11628~g;
  $$block11628~g: stack0o := TypeObject(ReturnFinally); goto $$block11628~f;
  $$block11628~f: assert (temp0 != null); goto $$block11628~e;
  $$block11628~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block11628~d;
  $$block11628~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block11628~c;
  $$block11628~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block11628~b;
  $$block11628~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block11628~a;
  $$block11628~a: assume IsHeap($Heap); goto block11560;
  block11441: goto block11458;
  block11560: goto block11577;
  block11458: goto block11339;
  block11577: goto block11594;
  block11339: goto block11356;
  block11594: goto block11322;
  block11356: return;
  block11322: goto block11339;
  
}

axiom (System.Type <: System.Type);
axiom (System.Reflection.MemberInfo <: System.Reflection.MemberInfo);
axiom ($BaseClass(System.Reflection.MemberInfo) == System.Object);
axiom ((System.Reflection.MemberInfo <: $BaseClass(System.Reflection.MemberInfo)) && (AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo));
axiom ($IsImmutable(System.Reflection.MemberInfo) && ($AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo));
axiom (System.Reflection.ICustomAttributeProvider <: System.Object);
axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider);
axiom (System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider);
axiom (System.Runtime.InteropServices._MemberInfo <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo);
axiom (System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo);
axiom $IsMemberlessType(System.Reflection.MemberInfo);
axiom ($BaseClass(System.Type) == System.Reflection.MemberInfo);
axiom ((System.Type <: $BaseClass(System.Type)) && (AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type));
axiom ($IsImmutable(System.Type) && ($AsImmutable(System.Type) == System.Type));
axiom (System.Runtime.InteropServices._Type <: System.Object);
axiom $IsMemberlessType(System.Runtime.InteropServices._Type);
axiom (System.Type <: System.Runtime.InteropServices._Type);
axiom (System.Reflection.IReflect <: System.Object);
axiom $IsMemberlessType(System.Reflection.IReflect);
axiom (System.Type <: System.Reflection.IReflect);
axiom $IsMemberlessType(System.Type);
axiom (Microsoft.Contracts.ICheckedException <: System.Object);
axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException);
procedure ReturnFinally.Expose1$System.Boolean(this : ref, b$in : bool where true);
  free requires true;
  requires !b$in;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.Expose1$System.Boolean(this : ref, b$in : bool) {
  var b : bool where true;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local13906 : ref where $Is(local13906, System.Exception);
  var stack0i : int;
  var stack0b : bool;
  var stack0o : ref;
  var stack0s : struct;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~j;
  $$entry~j: assume ($Heap[this, $allocated] == true); goto $$entry~i;
  $$entry~i: b := b$in; goto block12733;
  block12733: goto block13090;
  block13090: goto block13107;
  block13107: temp0 := this; goto $$block13107~j;
  $$block13107~j: havoc stack1s; goto $$block13107~i;
  $$block13107~i: assume $IsTokenForType(stack1s, ReturnFinally); goto $$block13107~h;
  $$block13107~h: stack1o := TypeObject(ReturnFinally); goto $$block13107~g;
  $$block13107~g: assert (temp0 != null); goto $$block13107~f;
  $$block13107~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: ReturnFinally)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block13107~e;
  $$block13107~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block13107~d;
  $$block13107~d: havoc temp1; goto $$block13107~c;
  $$block13107~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block13107~b;
  $$block13107~b: assume IsHeap($Heap); goto $$block13107~a;
  $$block13107~a: local13906 := null; goto block13124;
  block13124: stack0i := -4; goto $$block13124~d;
  $$block13124~d: assert (this != null); goto $$block13124~c;
  $$block13124~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block13124~b;
  $$block13124~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block13124~a;
  $$block13124~a: assume IsHeap($Heap); goto block13141;
  block13141: stack0b := b; goto true13141to13175, false13141to13158;
  true13141to13175: assume !stack0b; goto block13175;
  false13141to13158: assume stack0b; goto block13158;
  block13175: goto block13192;
  block13158: goto block13379;
  block13379: stack0o := null; goto true13379to13481, false13379to13396;
  true13379to13481: assume (local13906 == stack0o); goto block13481;
  false13379to13396: assume (local13906 != stack0o); goto block13396;
  block13481: goto block13498;
  block13396: goto true13396to13481, false13396to13413;
  block13192: goto block13209;
  true13396to13481: assume ($As(local13906, Microsoft.Contracts.ICheckedException) != null); goto block13481;
  false13396to13413: assume ($As(local13906, Microsoft.Contracts.ICheckedException) == null); goto block13413;
  block13413: goto block13430;
  block13209: stack0i := 2; goto $$block13209~d;
  $$block13209~d: assert (this != null); goto $$block13209~c;
  $$block13209~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block13209~b;
  $$block13209~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block13209~a;
  $$block13209~a: assume IsHeap($Heap); goto block13515;
  block13498: havoc stack0s; goto $$block13498~h;
  $$block13498~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block13498~g;
  $$block13498~g: stack0o := TypeObject(ReturnFinally); goto $$block13498~f;
  $$block13498~f: assert (temp0 != null); goto $$block13498~e;
  $$block13498~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block13498~d;
  $$block13498~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block13498~c;
  $$block13498~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block13498~b;
  $$block13498~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block13498~a;
  $$block13498~a: assume IsHeap($Heap); goto block13430;
  block13515: stack0o := null; goto true13515to13617, false13515to13532;
  true13515to13617: assume (local13906 == stack0o); goto block13617;
  false13515to13532: assume (local13906 != stack0o); goto block13532;
  block13617: goto block13634;
  block13532: goto true13532to13617, false13532to13549;
  block13430: goto block13447;
  true13532to13617: assume ($As(local13906, Microsoft.Contracts.ICheckedException) != null); goto block13617;
  false13532to13549: assume ($As(local13906, Microsoft.Contracts.ICheckedException) == null); goto block13549;
  block13549: goto block13566;
  block13447: goto block13464;
  block13634: havoc stack0s; goto $$block13634~h;
  $$block13634~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block13634~g;
  $$block13634~g: stack0o := TypeObject(ReturnFinally); goto $$block13634~f;
  $$block13634~f: assert (temp0 != null); goto $$block13634~e;
  $$block13634~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block13634~d;
  $$block13634~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block13634~c;
  $$block13634~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block13634~b;
  $$block13634~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block13634~a;
  $$block13634~a: assume IsHeap($Heap); goto block13566;
  block13464: goto block13345;
  block13566: goto block13583;
  block13345: goto block13362;
  block13583: goto block13600;
  block13362: return;
  block13600: goto block13328;
  block13328: goto block13345;
  
}

procedure ReturnFinally.Expose2$System.Boolean$System.Int32(this : ref, b$in : bool where true, x$in : int where InRange(x$in, System.Int32));
  free requires true;
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.Expose2$System.Boolean$System.Int32(this : ref, b$in : bool, x$in : int) {
  var b : bool where true;
  var x : int where InRange(x, System.Int32);
  var i : int where InRange(i, System.Int32);
  var stack0b : bool;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local15997 : ref where $Is(local15997, System.Exception);
  var stack0i : int;
  var stack0o : ref;
  var stack0s : struct;
  var local16014 : int where InRange(local16014, System.Int32);
  var $Heap$block15079$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~m;
  $$entry~m: assume ($Heap[this, $allocated] == true); goto $$entry~l;
  $$entry~l: b := b$in; goto $$entry~k;
  $$entry~k: x := x$in; goto block14790;
  block14790: goto block15045;
  block15045: goto block15062;
  block15062: i := 0; goto block15079$LoopPreheader;
  block15079: assume (((forall $o : ref :: (($Heap$block15079$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block15079$LoopPreheader[$ot, $allocated] == true) && ($Heap$block15079$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block15079$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block15079$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block15079$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block15079~d;
  $$block15079~d: assume (forall $o : ref :: ((($Heap$block15079$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block15079$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block15079$LoopPreheader[$o, $allocated] != true))); goto $$block15079~c;
  $$block15079~c: assume (forall $o : ref :: ((($Heap$block15079$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block15079~b;
  $$block15079~b: assert (forall $o : ref :: ((($o != null) && ($Heap$block15079$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block15079$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block15079$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block15079~a;
  $$block15079~a: assert (forall<$$tv~bf> $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> ($Heap$block15079$LoopPreheader[$o, $f] == $Heap[$o, $f]))); goto true15079to15385, false15079to15096;
  true15079to15385: assume (i >= x); goto block15385;
  false15079to15096: assume (i < x); goto block15096;
  block15385: goto block15402;
  block15096: temp0 := this; goto $$block15096~j;
  $$block15096~j: havoc stack1s; goto $$block15096~i;
  $$block15096~i: assume $IsTokenForType(stack1s, ReturnFinally); goto $$block15096~h;
  $$block15096~h: stack1o := TypeObject(ReturnFinally); goto $$block15096~g;
  $$block15096~g: assert (temp0 != null); goto $$block15096~f;
  $$block15096~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: ReturnFinally)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block15096~e;
  $$block15096~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block15096~d;
  $$block15096~d: havoc temp1; goto $$block15096~c;
  $$block15096~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block15096~b;
  $$block15096~b: assume IsHeap($Heap); goto $$block15096~a;
  $$block15096~a: local15997 := null; goto block15113;
  block15113: stack0i := -4; goto $$block15113~d;
  $$block15113~d: assert (this != null); goto $$block15113~c;
  $$block15113~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block15113~b;
  $$block15113~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block15113~a;
  $$block15113~a: assume IsHeap($Heap); goto block15130;
  block15402: goto block15419;
  block15130: stack0b := b; goto true15130to15164, false15130to15147;
  true15130to15164: assume !stack0b; goto block15164;
  false15130to15147: assume stack0b; goto block15147;
  block15164: goto block15181;
  block15147: goto block15436;
  block15419: return;
  block15181: goto block15198;
  block15436: stack0o := null; goto true15436to15538, false15436to15453;
  true15436to15538: assume (local15997 == stack0o); goto block15538;
  false15436to15453: assume (local15997 != stack0o); goto block15453;
  block15538: goto block15555;
  block15453: goto true15453to15538, false15453to15470;
  block15198: stack0i := 2; goto $$block15198~d;
  $$block15198~d: assert (this != null); goto $$block15198~c;
  $$block15198~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block15198~b;
  $$block15198~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block15198~a;
  $$block15198~a: assume IsHeap($Heap); goto block15572;
  true15453to15538: assume ($As(local15997, Microsoft.Contracts.ICheckedException) != null); goto block15538;
  false15453to15470: assume ($As(local15997, Microsoft.Contracts.ICheckedException) == null); goto block15470;
  block15470: goto block15487;
  block15572: stack0o := null; goto true15572to15674, false15572to15589;
  true15572to15674: assume (local15997 == stack0o); goto block15674;
  false15572to15589: assume (local15997 != stack0o); goto block15589;
  block15674: goto block15691;
  block15589: goto true15589to15674, false15589to15606;
  block15555: havoc stack0s; goto $$block15555~h;
  $$block15555~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block15555~g;
  $$block15555~g: stack0o := TypeObject(ReturnFinally); goto $$block15555~f;
  $$block15555~f: assert (temp0 != null); goto $$block15555~e;
  $$block15555~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block15555~d;
  $$block15555~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block15555~c;
  $$block15555~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block15555~b;
  $$block15555~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block15555~a;
  $$block15555~a: assume IsHeap($Heap); goto block15487;
  true15589to15674: assume ($As(local15997, Microsoft.Contracts.ICheckedException) != null); goto block15674;
  false15589to15606: assume ($As(local15997, Microsoft.Contracts.ICheckedException) == null); goto block15606;
  block15606: goto block15623;
  block15487: goto block15504;
  block15691: havoc stack0s; goto $$block15691~h;
  $$block15691~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block15691~g;
  $$block15691~g: stack0o := TypeObject(ReturnFinally); goto $$block15691~f;
  $$block15691~f: assert (temp0 != null); goto $$block15691~e;
  $$block15691~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block15691~d;
  $$block15691~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block15691~c;
  $$block15691~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block15691~b;
  $$block15691~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block15691~a;
  $$block15691~a: assume IsHeap($Heap); goto block15623;
  block15504: goto block15521;
  block15623: goto block15640;
  block15521: goto block15385;
  block15640: goto block15657;
  block15657: goto block15317;
  block15317: goto block15334;
  block15334: local16014 := i; goto $$block15334~d;
  $$block15334~d: stack0i := 1; goto $$block15334~c;
  $$block15334~c: stack0i := (local16014 + stack0i); goto $$block15334~b;
  $$block15334~b: i := stack0i; goto $$block15334~a;
  $$block15334~a: stack0i := local16014; goto block15351;
  block15351: goto block15368;
  block15368: goto block15079;
  block15079$LoopPreheader: $Heap$block15079$LoopPreheader := $Heap; goto block15079;
  
}

procedure ReturnFinally.Expose3$System.Boolean$System.Int32(this : ref, b$in : bool where true, x$in : int where InRange(x$in, System.Int32));
  free requires true;
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.Expose3$System.Boolean$System.Int32(this : ref, b$in : bool, x$in : int) {
  var b : bool where true;
  var x : int where InRange(x, System.Int32);
  var i : int where InRange(i, System.Int32);
  var stack0b : bool;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local18105 : ref where $Is(local18105, System.Exception);
  var stack0i : int;
  var stack0o : ref;
  var stack0s : struct;
  var local18156 : int where InRange(local18156, System.Int32);
  var $Heap$block17187$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~p;
  $$entry~p: assume ($Heap[this, $allocated] == true); goto $$entry~o;
  $$entry~o: b := b$in; goto $$entry~n;
  $$entry~n: x := x$in; goto block16898;
  block16898: goto block17153;
  block17153: goto block17170;
  block17170: i := 0; goto block17187$LoopPreheader;
  block17187: assume (((forall $o : ref :: (($Heap$block17187$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block17187$LoopPreheader[$ot, $allocated] == true) && ($Heap$block17187$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block17187$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block17187$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block17187$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block17187~d;
  $$block17187~d: assume (forall $o : ref :: ((($Heap$block17187$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block17187$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block17187$LoopPreheader[$o, $allocated] != true))); goto $$block17187~c;
  $$block17187~c: assume (forall $o : ref :: ((($Heap$block17187$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block17187~b;
  $$block17187~b: assert (forall $o : ref :: ((($o != null) && ($Heap$block17187$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block17187$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block17187$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block17187~a;
  $$block17187~a: assert (forall<$$tv~bn> $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> ($Heap$block17187$LoopPreheader[$o, $f] == $Heap[$o, $f]))); goto true17187to17493, false17187to17204;
  true17187to17493: assume (i >= x); goto block17493;
  false17187to17204: assume (i < x); goto block17204;
  block17493: goto block17510;
  block17204: temp0 := this; goto $$block17204~j;
  $$block17204~j: havoc stack1s; goto $$block17204~i;
  $$block17204~i: assume $IsTokenForType(stack1s, ReturnFinally); goto $$block17204~h;
  $$block17204~h: stack1o := TypeObject(ReturnFinally); goto $$block17204~g;
  $$block17204~g: assert (temp0 != null); goto $$block17204~f;
  $$block17204~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: ReturnFinally)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block17204~e;
  $$block17204~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block17204~d;
  $$block17204~d: havoc temp1; goto $$block17204~c;
  $$block17204~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block17204~b;
  $$block17204~b: assume IsHeap($Heap); goto $$block17204~a;
  $$block17204~a: local18105 := null; goto block17221;
  block17510: goto block17527;
  block17221: stack0i := -4; goto $$block17221~d;
  $$block17221~d: assert (this != null); goto $$block17221~c;
  $$block17221~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block17221~b;
  $$block17221~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block17221~a;
  $$block17221~a: assume IsHeap($Heap); goto block17238;
  block17527: return;
  block17238: stack0b := b; goto true17238to17272, false17238to17255;
  true17238to17272: assume !stack0b; goto block17272;
  false17238to17255: assume stack0b; goto block17255;
  block17272: goto block17289;
  block17255: goto block17544;
  block17289: goto block17306;
  block17544: stack0o := null; goto true17544to17646, false17544to17561;
  true17544to17646: assume (local18105 == stack0o); goto block17646;
  false17544to17561: assume (local18105 != stack0o); goto block17561;
  block17646: goto block17663;
  block17561: goto true17561to17646, false17561to17578;
  block17306: stack0i := 2; goto $$block17306~d;
  $$block17306~d: assert (this != null); goto $$block17306~c;
  $$block17306~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block17306~b;
  $$block17306~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block17306~a;
  $$block17306~a: assume IsHeap($Heap); goto block17680;
  true17561to17646: assume ($As(local18105, Microsoft.Contracts.ICheckedException) != null); goto block17646;
  false17561to17578: assume ($As(local18105, Microsoft.Contracts.ICheckedException) == null); goto block17578;
  block17578: goto block17595;
  block17680: stack0o := null; goto true17680to17782, false17680to17697;
  true17680to17782: assume (local18105 == stack0o); goto block17782;
  false17680to17697: assume (local18105 != stack0o); goto block17697;
  block17782: goto block17799;
  block17697: goto true17697to17782, false17697to17714;
  block17663: havoc stack0s; goto $$block17663~h;
  $$block17663~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block17663~g;
  $$block17663~g: stack0o := TypeObject(ReturnFinally); goto $$block17663~f;
  $$block17663~f: assert (temp0 != null); goto $$block17663~e;
  $$block17663~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block17663~d;
  $$block17663~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block17663~c;
  $$block17663~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block17663~b;
  $$block17663~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block17663~a;
  $$block17663~a: assume IsHeap($Heap); goto block17595;
  true17697to17782: assume ($As(local18105, Microsoft.Contracts.ICheckedException) != null); goto block17782;
  false17697to17714: assume ($As(local18105, Microsoft.Contracts.ICheckedException) == null); goto block17714;
  block17714: goto block17731;
  block17595: goto block17612;
  block17799: havoc stack0s; goto $$block17799~h;
  $$block17799~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block17799~g;
  $$block17799~g: stack0o := TypeObject(ReturnFinally); goto $$block17799~f;
  $$block17799~f: assert (temp0 != null); goto $$block17799~e;
  $$block17799~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block17799~d;
  $$block17799~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block17799~c;
  $$block17799~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block17799~b;
  $$block17799~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block17799~a;
  $$block17799~a: assume IsHeap($Heap); goto block17731;
  block17612: goto block17629;
  block17731: goto block17748;
  block17629: goto block17442;
  block17748: goto block17765;
  block17442: local18156 := i; goto $$block17442~d;
  $$block17442~d: stack0i := 1; goto $$block17442~c;
  $$block17442~c: stack0i := (local18156 + stack0i); goto $$block17442~b;
  $$block17442~b: i := stack0i; goto $$block17442~a;
  $$block17442~a: stack0i := local18156; goto block17459;
  block17765: goto block17425;
  block17459: goto block17476;
  block17425: goto block17442;
  block17476: goto block17187;
  block17187$LoopPreheader: $Heap$block17187$LoopPreheader := $Heap; goto block17187;
  
}

procedure ReturnFinally.Expose4$System.Boolean$System.Int32(this : ref, b$in : bool where true, x$in : int where InRange(x$in, System.Int32));
  free requires true;
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.Expose4$System.Boolean$System.Int32(this : ref, b$in : bool, x$in : int) {
  var b : bool where true;
  var x : int where InRange(x, System.Int32);
  var i : int where InRange(i, System.Int32);
  var stack0b : bool;
  var temp0 : ref;
  var stack1s : struct;
  var stack1o : ref;
  var temp1 : exposeVersionType;
  var local20247 : ref where $Is(local20247, System.Exception);
  var stack0i : int;
  var stack0o : ref;
  var stack0s : struct;
  var local20264 : int where InRange(local20264, System.Int32);
  var $Heap$block19312$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~s;
  $$entry~s: assume ($Heap[this, $allocated] == true); goto $$entry~r;
  $$entry~r: b := b$in; goto $$entry~q;
  $$entry~q: x := x$in; goto block19023;
  block19023: goto block19278;
  block19278: goto block19295;
  block19295: i := 0; goto block19312$LoopPreheader;
  block19312: assume (((forall $o : ref :: (($Heap$block19312$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block19312$LoopPreheader[$ot, $allocated] == true) && ($Heap$block19312$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block19312$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block19312$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block19312$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block19312~d;
  $$block19312~d: assume (forall $o : ref :: ((($Heap$block19312$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block19312$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block19312$LoopPreheader[$o, $allocated] != true))); goto $$block19312~c;
  $$block19312~c: assume (forall $o : ref :: ((($Heap$block19312$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block19312~b;
  $$block19312~b: assert (forall $o : ref :: ((($o != null) && ($Heap$block19312$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block19312$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block19312$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block19312~a;
  $$block19312~a: assert (forall<$$tv~bt> $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old((($o != this) || ($f != ReturnFinally.y)))) && old((($o != this) || ($f != $exposeVersion)))) ==> ($Heap$block19312$LoopPreheader[$o, $f] == $Heap[$o, $f]))); goto true19312to19618, false19312to19329;
  true19312to19618: assume (i >= x); goto block19618;
  false19312to19329: assume (i < x); goto block19329;
  block19618: goto block19635;
  block19329: temp0 := this; goto $$block19329~j;
  $$block19329~j: havoc stack1s; goto $$block19329~i;
  $$block19329~i: assume $IsTokenForType(stack1s, ReturnFinally); goto $$block19329~h;
  $$block19329~h: stack1o := TypeObject(ReturnFinally); goto $$block19329~g;
  $$block19329~g: assert (temp0 != null); goto $$block19329~f;
  $$block19329~f: assert ((((($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame])) || ($Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame]))) && ($Heap[temp0, $inv] <: ReturnFinally)) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block19329~e;
  $$block19329~e: $Heap := $Heap[temp0, $localinv := System.Object]; goto $$block19329~d;
  $$block19329~d: havoc temp1; goto $$block19329~c;
  $$block19329~c: $Heap := $Heap[temp0, $exposeVersion := temp1]; goto $$block19329~b;
  $$block19329~b: assume IsHeap($Heap); goto $$block19329~a;
  $$block19329~a: local20247 := null; goto block19346;
  block19635: goto block19652;
  block19346: stack0i := -4; goto $$block19346~d;
  $$block19346~d: assert (this != null); goto $$block19346~c;
  $$block19346~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block19346~b;
  $$block19346~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block19346~a;
  $$block19346~a: assume IsHeap($Heap); goto block19363;
  block19652: goto block19669;
  block19363: stack0b := b; goto true19363to19397, false19363to19380;
  true19363to19397: assume !stack0b; goto block19397;
  false19363to19380: assume stack0b; goto block19380;
  block19397: goto block19414;
  block19380: goto block19686;
  block19669: return;
  block19414: goto block19431;
  block19686: stack0o := null; goto true19686to19788, false19686to19703;
  true19686to19788: assume (local20247 == stack0o); goto block19788;
  false19686to19703: assume (local20247 != stack0o); goto block19703;
  block19788: goto block19805;
  block19703: goto true19703to19788, false19703to19720;
  block19431: stack0i := 2; goto $$block19431~d;
  $$block19431~d: assert (this != null); goto $$block19431~c;
  $$block19431~c: assert (!($Heap[this, $inv] <: ReturnFinally) || ($Heap[this, $localinv] == System.Object)); goto $$block19431~b;
  $$block19431~b: $Heap := $Heap[this, ReturnFinally.y := stack0i]; goto $$block19431~a;
  $$block19431~a: assume IsHeap($Heap); goto block19822;
  true19703to19788: assume ($As(local20247, Microsoft.Contracts.ICheckedException) != null); goto block19788;
  false19703to19720: assume ($As(local20247, Microsoft.Contracts.ICheckedException) == null); goto block19720;
  block19720: goto block19737;
  block19822: stack0o := null; goto true19822to19924, false19822to19839;
  true19822to19924: assume (local20247 == stack0o); goto block19924;
  false19822to19839: assume (local20247 != stack0o); goto block19839;
  block19924: goto block19941;
  block19839: goto true19839to19924, false19839to19856;
  block19805: havoc stack0s; goto $$block19805~h;
  $$block19805~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block19805~g;
  $$block19805~g: stack0o := TypeObject(ReturnFinally); goto $$block19805~f;
  $$block19805~f: assert (temp0 != null); goto $$block19805~e;
  $$block19805~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block19805~d;
  $$block19805~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block19805~c;
  $$block19805~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block19805~b;
  $$block19805~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block19805~a;
  $$block19805~a: assume IsHeap($Heap); goto block19737;
  true19839to19924: assume ($As(local20247, Microsoft.Contracts.ICheckedException) != null); goto block19924;
  false19839to19856: assume ($As(local20247, Microsoft.Contracts.ICheckedException) == null); goto block19856;
  block19856: goto block19873;
  block19737: goto block19754;
  block19941: havoc stack0s; goto $$block19941~h;
  $$block19941~h: assume $IsTokenForType(stack0s, ReturnFinally); goto $$block19941~g;
  $$block19941~g: stack0o := TypeObject(ReturnFinally); goto $$block19941~f;
  $$block19941~f: assert (temp0 != null); goto $$block19941~e;
  $$block19941~e: assert ($Heap[temp0, $localinv] == System.Object); goto $$block19941~d;
  $$block19941~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block19941~c;
  $$block19941~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block19941~b;
  $$block19941~b: $Heap := $Heap[temp0, $localinv := $typeof(temp0)]; goto $$block19941~a;
  $$block19941~a: assume IsHeap($Heap); goto block19873;
  block19754: goto block19771;
  block19873: goto block19890;
  block19771: goto block19635;
  block19890: goto block19907;
  block19907: goto block19550;
  block19550: goto block19567;
  block19567: local20264 := i; goto $$block19567~d;
  $$block19567~d: stack0i := 1; goto $$block19567~c;
  $$block19567~c: stack0i := (local20264 + stack0i); goto $$block19567~b;
  $$block19567~b: i := stack0i; goto $$block19567~a;
  $$block19567~a: stack0i := local20264; goto block19584;
  block19584: goto block19601;
  block19601: goto block19312;
  block19312$LoopPreheader: $Heap$block19312$LoopPreheader := $Heap; goto block19312;
  
}

procedure ReturnFinally.M(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.M(this : ref) {
  var stack0o : ref;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~t;
  $$entry~t: assume ($Heap[this, $allocated] == true); goto block21029;
  block21029: goto block21284;
  block21284: goto block21301;
  block21301: goto block21403;
  block21403: assert false; return;
  
}

procedure ReturnFinally.N(this : ref);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.N(this : ref) {
  var stack0o : ref;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~u;
  $$entry~u: assume ($Heap[this, $allocated] == true); goto block22355;
  block22355: goto block22610;
  block22610: goto block22627;
  block22627: goto block22746;
  block22746: assert false; return;
  
}

procedure ReturnFinally.P0$System.Int32(this : ref, x$in : int where InRange(x$in, System.Int32));
  free requires true;
  requires (0 <= x$in);
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.P0$System.Int32(this : ref, x$in : int) {
  var x : int where InRange(x, System.Int32);
  var stack0o : ref;
  var stack0i : int;
  var stack0b : bool;
  var local24922 : int where InRange(local24922, System.Int32);
  var $Heap$block24531$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~w;
  $$entry~w: assume ($Heap[this, $allocated] == true); goto $$entry~v;
  $$entry~v: x := x$in; goto block24055;
  block24055: goto block24412;
  block24412: goto block24429;
  block24429: goto block24531$LoopPreheader;
  block24531: assume (((forall $o : ref :: (($Heap$block24531$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block24531$LoopPreheader[$ot, $allocated] == true) && ($Heap$block24531$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block24531$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block24531$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block24531$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block24531~e;
  $$block24531~e: assume (forall $o : ref :: ((($Heap$block24531$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block24531$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block24531$LoopPreheader[$o, $allocated] != true))); goto $$block24531~d;
  $$block24531~d: assume (forall $o : ref :: ((($Heap$block24531$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block24531~c;
  $$block24531~c: assert (forall $o : ref :: ((($o != null) && ($Heap$block24531$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block24531$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block24531$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block24531~b;
  $$block24531~b: assert (forall<$$tv~cl> $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> ($Heap$block24531$LoopPreheader[$o, $f] == $Heap[$o, $f]))); goto $$block24531~a;
  $$block24531~a: assert (0 <= x); goto block24616;
  block24616: goto block24633;
  block24633: stack0i := 0; goto true24633to24701, false24633to24650;
  true24633to24701: assume (stack0i >= x); goto block24701;
  false24633to24650: assume (stack0i < x); goto block24650;
  block24701: goto block24718;
  block24650: local24922 := x; goto $$block24650~d;
  $$block24650~d: stack0i := 1; goto $$block24650~c;
  $$block24650~c: stack0i := (local24922 - stack0i); goto $$block24650~b;
  $$block24650~b: x := stack0i; goto $$block24650~a;
  $$block24650~a: stack0i := local24922; goto block24667;
  block24718: goto block24480;
  block24667: goto block24684;
  block24480: goto block24497;
  block24684: goto block24531;
  block24497: goto block24514;
  block24514: return;
  block24531$LoopPreheader: $Heap$block24531$LoopPreheader := $Heap; goto block24531;
  
}

procedure ReturnFinally.P1$System.Int32(this : ref, x$in : int where InRange(x$in, System.Int32));
  free requires true;
  requires (((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && (forall $pc : ref :: ((((($pc != null) && ($Heap[$pc, $allocated] == true)) && ($Heap[$pc, $ownerRef] == $Heap[this, $ownerRef])) && ($Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame])) ==> (($Heap[$pc, $inv] == $typeof($pc)) && ($Heap[$pc, $localinv] == $typeof($pc))))));
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally.P1$System.Int32(this : ref, x$in : int) {
  var x : int where InRange(x, System.Int32);
  var stack0o : ref;
  var stack0i : int;
  var stack0b : bool;
  var local26571 : int where InRange(local26571, System.Int32);
  var $Heap$block26180$LoopPreheader : <x>[ref, name]x;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~y;
  $$entry~y: assume ($Heap[this, $allocated] == true); goto $$entry~x;
  $$entry~x: x := x$in; goto block25806;
  block25806: goto block26061;
  block26061: goto block26078;
  block26078: goto block26180$LoopPreheader;
  block26180: assume (((forall $o : ref :: (($Heap$block26180$LoopPreheader[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: ((($Heap$block26180$LoopPreheader[$ot, $allocated] == true) && ($Heap$block26180$LoopPreheader[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == $Heap$block26180$LoopPreheader[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == $Heap$block26180$LoopPreheader[$ot, $ownerFrame]))))) && ($Heap$block26180$LoopPreheader[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized])); goto $$block26180~e;
  $$block26180~e: assume (forall $o : ref :: ((($Heap$block26180$LoopPreheader[$o, $inv] == $Heap[$o, $inv]) && ($Heap$block26180$LoopPreheader[$o, $localinv] == $Heap[$o, $localinv])) || ($Heap$block26180$LoopPreheader[$o, $allocated] != true))); goto $$block26180~d;
  $$block26180~d: assume (forall $o : ref :: ((($Heap$block26180$LoopPreheader[$o, $allocated] != true) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o))))); goto $$block26180~c;
  $$block26180~c: assert (forall $o : ref :: ((($o != null) && ($Heap$block26180$LoopPreheader[$o, $allocated] == true)) ==> (($Heap$block26180$LoopPreheader[$o, $ownerRef] == $Heap[$o, $ownerRef]) && ($Heap$block26180$LoopPreheader[$o, $ownerFrame] == $Heap[$o, $ownerFrame])))); goto $$block26180~b;
  $$block26180~b: assert (forall<$$tv~cs> $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old((($o != this) || ($f != $exposeVersion)))) ==> ($Heap$block26180$LoopPreheader[$o, $f] == $Heap[$o, $f]))); goto $$block26180~a;
  $$block26180~a: assert (0 <= x); goto block26265;
  block26265: goto block26282;
  block26282: stack0i := 0; goto true26282to26350, false26282to26299;
  true26282to26350: assume (stack0i >= x); goto block26350;
  false26282to26299: assume (stack0i < x); goto block26299;
  block26350: goto block26367;
  block26299: local26571 := x; goto $$block26299~d;
  $$block26299~d: stack0i := 1; goto $$block26299~c;
  $$block26299~c: stack0i := (local26571 - stack0i); goto $$block26299~b;
  $$block26299~b: x := stack0i; goto $$block26299~a;
  $$block26299~a: stack0i := local26571; goto block26316;
  block26367: goto block26129;
  block26316: goto block26333;
  block26129: goto block26146;
  block26333: goto block26180;
  block26146: goto block26163;
  block26163: return;
  block26180$LoopPreheader: $Heap$block26180$LoopPreheader := $Heap; goto block26180;
  
}

procedure ReturnFinally..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == ReturnFinally)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(ReturnFinally <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

implementation ReturnFinally..ctor(this : ref) {
  var temp0 : ref;
  entry: assume $IsNotNull(this, ReturnFinally); goto $$entry~ab;
  $$entry~ab: assume ($Heap[this, $allocated] == true); goto $$entry~aa;
  $$entry~aa: assume ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this))); goto $$entry~z;
  $$entry~z: assume ($Heap[this, ReturnFinally.y] == 0); goto block27030;
  block27030: goto block27047;
  block27047: goto block27064;
  block27064: assert (this != null); goto $$block27064~a;
  $$block27064~a: call System.Object..ctor(this); goto block27183;
  block27183: goto block27200;
  block27200: goto block27217;
  block27217: goto block27234;
  block27234: temp0 := this; goto $$block27234~f;
  $$block27234~f: assert (temp0 != null); goto $$block27234~e;
  $$block27234~e: assert (($Heap[temp0, $inv] == System.Object) && ($Heap[temp0, $localinv] == $typeof(temp0))); goto $$block27234~d;
  $$block27234~d: assert (0 <= $Heap[temp0, ReturnFinally.y]); goto $$block27234~c;
  $$block27234~c: assert (forall $p : ref :: ((((($p != null) && ($Heap[$p, $allocated] == true)) && ($Heap[$p, $ownerRef] == temp0)) && ($Heap[$p, $ownerFrame] == ReturnFinally)) ==> (($Heap[$p, $inv] == $typeof($p)) && ($Heap[$p, $localinv] == $typeof($p))))); goto $$block27234~b;
  $$block27234~b: $Heap := $Heap[temp0, $inv := ReturnFinally]; goto $$block27234~a;
  $$block27234~a: assume IsHeap($Heap); return;
  
}

procedure System.Object..ctor(this : ref);
  free requires (forall $o : ref :: (($o != this) ==> ($Heap[$o, $ownerRef] != this)));
  free requires (($Heap[this, $ownerRef] == this) && ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder));
  free requires (forall $o : ref :: ((($Heap[$o, $ownerRef] == $Heap[this, $ownerRef]) && ($Heap[$o, $ownerFrame] == $Heap[this, $ownerFrame])) ==> ($o == this)));
  free requires ($BeingConstructed == this);
  modifies $Heap;
  ensures ((((($Heap[this, $ownerFrame] == $PeerGroupPlaceholder) || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame])) || ($Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]))) && ($Heap[this, $inv] == System.Object)) && ($Heap[this, $localinv] == $typeof(this)));
  ensures (($Heap[this, $ownerRef] == old($Heap)[this, $ownerRef]) && ($Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]));
  ensures ($Heap[this, $sharingMode] == $SharingMode_Unshared);
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && (($o != this) || !(System.Object <: DeclType($f)))) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: ((($o == this) || ((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv]))) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (($o == this) || (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode])));
  

procedure ReturnFinally..cctor();
  free requires ($BeingConstructed == null);
  modifies $Heap;
  free ensures (forall $o : ref :: (((($o != null) && (old($Heap)[$o, $allocated] != true)) && ($Heap[$o, $allocated] == true)) ==> (($Heap[$o, $inv] == $typeof($o)) && ($Heap[$o, $localinv] == $typeof($o)))));
  free ensures (forall $o : ref :: {$Heap[$o, $FirstConsistentOwner]} ((old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion]) ==> (old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner])));
  ensures (forall $o : ref :: ((($o != null) && (old($Heap)[$o, $allocated] == true)) ==> ((old($Heap)[$o, $ownerRef] == $Heap[$o, $ownerRef]) && (old($Heap)[$o, $ownerFrame] == $Heap[$o, $ownerFrame]))));
  free ensures (forall $o : ref, $f : name :: {$Heap[$o, $f]} (((((((((($f != $inv) && ($f != $localinv)) && ($f != $FirstConsistentOwner)) && (!IsStaticField($f) || !IsDirectlyModifiableField($f))) && ($o != null)) && (old($Heap)[$o, $allocated] == true)) && (((old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder) || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame])) || (old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])))) && old(true)) && old(true)) ==> (old($Heap)[$o, $f] == $Heap[$o, $f])));
  free ensures (forall $o : ref :: (((old($Heap)[$o, $inv] == $Heap[$o, $inv]) && (old($Heap)[$o, $localinv] == $Heap[$o, $localinv])) || (old($Heap)[$o, $allocated] != true)));
  free ensures (((forall $o : ref :: ((old($Heap)[$o, $allocated] == true) ==> ($Heap[$o, $allocated] == true))) && (forall $ot : ref :: (((old($Heap)[$ot, $allocated] == true) && (old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder)) ==> (($Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef]) && ($Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]))))) && (old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]));
  free ensures (forall $o : ref :: (old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]));
  

implementation ReturnFinally..cctor() {
  entry: goto block27574;
  block27574: goto block27693;
  block27693: goto block27710;
  block27710: goto block27727;
  block27727: return;
  
}

